(declare-fun v1 () Bool)
(declare-fun v2 () Bool)
(declare-const v1 Bool)
(declare-const v4 Bool)
(declare-const i5 Int)
(declare-const i8 Int)
(push)
(assert (or v2 (and v1 (= v4 (not (= (- i8 i5 i5 1) (mod (- i8 i5 i5 1) 5)))) (= v1 v4) (= v4 (> (- i8 i5 i5) 1)))))
(check-sat)
(check-sat)
